D:Dsys.
Feasible(D)
 (i:Id, l:IdLnk, tg:Id.
 (if destination(l) = i M(source(l)).dout(l,tg) else Void fi  M(i).da(rcv(l,tg))) 

latex

Definitions	if b t else f fi, Feasible(D), Unit, P  Q, P & Q, P  Q, , Prop, t  T, x:A. B(x), M.da(a)
Lemmas	rcv wf, d-m wf, ma-da wf, lsrc wf, ma-dout wf, ldst wf, Id wf, assert wf, bool wf, eq id wf, eqff to assert, assert-eq-id, eqtt to assert, iff transitivity, dsys wf, d-feasible wf, IdLnk wf